<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
"http://www.w3.org/TR/html4/loose.dtd">

<html>
<head>

<title>
PRISM Manual | ThePRISMLanguage / Example1 
</title>

<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<meta name="keywords" content="prism, probabilistic, symbolic, model, checker, verification, birmingham, oxford, parker, norman, kwiatkowska">

<link rel="icon" href="../pub/skins/offline/images/p16.ico" type="image/x-icon">
<link rel="shortcut icon" href="../pub/skins/offline/images/p16.ico" type="image/x-icon">

<!--HTMLHeader--><style type='text/css'><!--
  ul, ol, pre, dl, p { margin-top:0px; margin-bottom:0px; }
  code.escaped { white-space: nowrap; }
  .vspace { margin-top:1.33em; }
  .indent { margin-left:40px; }
  .outdent { margin-left:40px; text-indent:-40px; }
  a.createlinktext { text-decoration:none; border-bottom:1px dotted gray; }
  a.createlink { text-decoration:none; position:relative; top:-0.5em;
    font-weight:bold; font-size:smaller; border-bottom:none; }
  img { border:0px; }
  .editconflict { color:green; 
  font-style:italic; margin-top:1.33em; margin-bottom:1.33em; }

  table.markup { border:2px dotted #ccf; width:90%; }
  td.markup1, td.markup2 { padding-left:10px; padding-right:10px; }
  table.vert td.markup1 { border-bottom:1px solid #ccf; }
  table.horiz td.markup1 { width:23em; border-right:1px solid #ccf; }
  table.markup caption { text-align:left; }
  div.faq p, div.faq pre { margin-left:2em; }
  div.faq p.question { margin:1em 0 0.75em 0; font-weight:bold; }
  div.faqtoc div.faq * { display:none; }
  div.faqtoc div.faq p.question 
    { display:block; font-weight:normal; margin:0.5em 0 0.5em 20px; line-height:normal; }
  div.faqtoc div.faq p.question * { display:inline; }
   
    .frame 
      { border:1px solid #cccccc; padding:4px; background-color:#f9f9f9; }
    .lfloat { float:left; margin-right:0.5em; }
    .rfloat { float:right; margin-left:0.5em; }
a.varlink { text-decoration:none; }

.sourceblocklink {
  text-align: right;
  font-size: smaller;
}
.sourceblocktext {
  padding: 0.5em;
  border: 1px solid #808080;
  color: #000000;
  background-color: #f1f0ed;
}
.sourceblocktext div {
  font-family: monospace;
  font-size: small;
  line-height: 1;
  height: 1%;
}
.sourceblocktext div.head,
.sourceblocktext div.foot {
  font: italic medium serif;
  padding: 0.5em;
}

--></style>  <meta name='robots' content='index,follow' />


<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/base.css">
<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/prism.css">
<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/prismmanual.css">

</head>

<body text="#000000" bgcolor="#ffffff">

<div id="layout-maincontainer">
<div id="layout-main">

<div id="prism-mainbox">

<!-- ============================================================================= -->

<!--PageHeaderFmt-->
<!--/PageHeaderFmt-->

<!--PageTitleFmt-->
  <div id="prism-man-title">
    <p><a class='wikilink' href='Introduction.html'>The PRISM Language</a> /
</p><h1>Example 1</h1>

  </div>
<!--PageText-->
<div id='wikitext'>
<p>We will use the following simple example to illustrate the basic concepts of the PRISM language.
Consider a system comprising two identical processes which must operate under mutual exclusion.
Each process can be in one of 3 states: {0,1,2}.
From state 0, a process will move to state 1 with probability 0.2
and remain in the same state with probability 0.8.
From state 1, it tries to move to the critical section: state 2.
This can only occur if the other process is not in its critical section.
Finally, from state 2, a process will either remain there or move back to state 0
with equal probability.
The PRISM code to describe an MDP model of this system can be seen below.
In the next sections, we explain each aspect of the code in turn.
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock1'>
  <div class='sourceblocktext'><div class="prism"><span class="prismcomment">// Example 1</span><br/>
<span class="prismcomment">// Two process mutual exclusion</span><br/>
<br/>
<span class="prismkeyword">mdp</span><br/>
<br/>
<span class="prismkeyword">module</span> <span class="prismident">M1</span><br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="prismident">x</span> : [<span class="prismnum">0</span>..<span class="prismnum">2</span>] <span class="prismkeyword">init</span> <span class="prismnum">0</span>;<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;[] <span class="prismident">x</span>=<span class="prismnum">0</span> -&gt; <span class="prismnum">0.8</span>:(<span class="prismident">x</span>'=<span class="prismnum">0</span>) + <span class="prismnum">0.2</span>:(<span class="prismident">x</span>'=<span class="prismnum">1</span>);<br/>
&nbsp;&nbsp;&nbsp;&nbsp;[] <span class="prismident">x</span>=<span class="prismnum">1</span> &amp; <span class="prismident">y</span>!=<span class="prismnum">2</span> -&gt; (<span class="prismident">x</span>'=<span class="prismnum">2</span>);<br/>
&nbsp;&nbsp;&nbsp;&nbsp;[] <span class="prismident">x</span>=<span class="prismnum">2</span> -&gt; <span class="prismnum">0.5</span>:(<span class="prismident">x</span>'=<span class="prismnum">2</span>) + <span class="prismnum">0.5</span>:(<span class="prismident">x</span>'=<span class="prismnum">0</span>);<br/>
<br/>
<span class="prismkeyword">endmodule</span><br/>
<br/>
<span class="prismkeyword">module</span> <span class="prismident">M2</span><br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="prismident">y</span> : [<span class="prismnum">0</span>..<span class="prismnum">2</span>] <span class="prismkeyword">init</span> <span class="prismnum">0</span>;<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;[] <span class="prismident">y</span>=<span class="prismnum">0</span> -&gt; <span class="prismnum">0.8</span>:(<span class="prismident">y</span>'=<span class="prismnum">0</span>) + <span class="prismnum">0.2</span>:(<span class="prismident">y</span>'=<span class="prismnum">1</span>);<br/>
&nbsp;&nbsp;&nbsp;&nbsp;[] <span class="prismident">y</span>=<span class="prismnum">1</span> &amp; <span class="prismident">x</span>!=<span class="prismnum">2</span> -&gt; (<span class="prismident">y</span>'=<span class="prismnum">2</span>);<br/>
&nbsp;&nbsp;&nbsp;&nbsp;[] <span class="prismident">y</span>=<span class="prismnum">2</span> -&gt; <span class="prismnum">0.5</span>:(<span class="prismident">y</span>'=<span class="prismnum">2</span>) + <span class="prismnum">0.5</span>:(<span class="prismident">y</span>'=<span class="prismnum">0</span>);<br/>
<br/>
<span class="prismkeyword">endmodule</span><br/>
</div></div>
  <div class='sourceblocklink'><a href='Example1@action=sourceblock&amp;num=1' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'  style='text-align: center;'><strong>The PRISM Language: Example 1</strong>
</p>
</div>


<!--PageFooterFmt-->
  <div id='prism-man-footer'>
  </div>
<!--/PageFooterFmt-->


<!-- ============================================================================= -->

</div> <!-- id="prism-mainbox" -->

</div> <!-- id="layout-main" -->
</div> <!-- id="layout-maincontainer" -->

<div id="layout-leftcol">
<div id="prism-navbar2">

<h3><a class='wikilink' href='../Main/Welcome.html'>PRISM Manual</a></h3>
<p><strong><a class='wikilink' href='Introduction.html'>The PRISM Language</a></strong>
</p><ul><li><a class='wikilink' href='Introduction.html'>Introduction</a>
</li><li><a class='selflink' href='Example1.html'>Example 1</a>
</li><li><a class='wikilink' href='ModelType.html'>Model Type</a>
</li><li><a class='wikilink' href='ModulesAndVariables.html'>Modules And Variables</a>
</li><li><a class='wikilink' href='Commands.html'>Commands</a>
</li><li><a class='wikilink' href='ParallelComposition.html'>Parallel Composition</a>
</li><li><a class='wikilink' href='LocalNondeterminism.html'>Local Nondeterminism</a>
</li><li><a class='wikilink' href='CTMCs.html'>CTMCs</a>
</li><li><a class='wikilink' href='Example2.html'>Example 2</a>
</li><li><a class='wikilink' href='Constants.html'>Constants</a>
</li><li><a class='wikilink' href='Expressions.html'>Expressions</a>
</li><li><a class='wikilink' href='Synchronisation.html'>Synchronisation</a>
</li><li><a class='wikilink' href='ModuleRenaming.html'>Module Renaming</a>
</li><li><a class='wikilink' href='MultipleInitialStates.html'>Multiple Initial States</a>
</li><li><a class='wikilink' href='GlobalVariables.html'>Global Variables</a>
</li><li><a class='wikilink' href='FormulasAndLabels.html'>Formulas And Labels</a>
</li><li><a class='wikilink' href='PTAs.html'>PTAs</a>
</li><li><a class='wikilink' href='CostsAndRewards.html'>Costs And Rewards</a>
</li><li><a class='wikilink' href='ProcessAlgebraOperators.html'>Process Algebra Operators</a>
</li><li><a class='wikilink' href='PRISMModelFiles.html'>PRISM Model Files</a>
</li></ul><p>[ <a class='wikilink' href='AllOnOnePage.html'>View all</a> ]
</p>


</div>  <!-- id="prism-navbar2" -->
</div> <!-- id="layout-leftcol" -->

</body>
</html>
